/-
Copyright (c) 2025 Floris van Doorn and Hannah Scholz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Hannah Scholz
-/
module

public import Mathlib.Topology.Coherent
public import Mathlib.Topology.Compactness.Compact

/-!
# Compactly coherent spaces and the k-ification

In this file we will define compactly coherent spaces and prove basic properties about them.
This is a weaker version of `CompactlyGeneratedSpace`. These notions agree on Hausdorff spaces. They
are both referred to as compactly generated spaces in the literature.

## Main definitions
* `CompactlyCoherentSpace`: A compactly coherent space is a topological space in which a set `A` is
  open iff for every compact set `B`, the intersection `A ∩ B` is open in `B`.

## Main results
* `CompactlyCoherentSpace.of_weaklyLocallyCompactSpace`: every weakly locally compact space is a
  compactly coherent space.
* `CompactlyCoherentSpace.of_sequentialSpace`: every sequential space is a compactly coherent space.

## References
* [J. Munkres, *Topology*][Munkres2000]
* <https://en.wikipedia.org/wiki/Compactly_generated_space>
-/

@[expose] public section

noncomputable section

open Set Set.Notation Topology

/-! ### Compactly coherent spaces-/

/-- A space is a compactly coherent space if the topology is generated by the compact sets. -/
class CompactlyCoherentSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- A space is a compactly coherent space if the topology is generated by the compact sets. -/
  isCoherentWith : IsCoherentWith (X := X) {K | IsCompact K}

namespace CompactlyCoherentSpace

universe u

variable {X : Type u} [TopologicalSpace X]

/-- A set `A` in a compactly coherent space is open iff for every compact set `K`, the intersection
`K ∩ A` is open in `K`. -/
lemma isOpen_iff [CompactlyCoherentSpace X] {A : Set X} :
    IsOpen A ↔ ∀ K, IsCompact K → IsOpen (K ↓∩ A) :=
  IsCoherentWith.isOpen_iff isCoherentWith

/-- A set `A` in a compactly coherent space is closed iff for every compact set `K`, the
intersection `K ∩ A` is closed in `K`. -/
lemma isClosed_iff [CompactlyCoherentSpace X] (A : Set X) :
    IsClosed A ↔ ∀ K, IsCompact K → IsClosed (K ↓∩ A) :=
  IsCoherentWith.isClosed_iff isCoherentWith

/-- If every set `A` is open if for every compact `K` the intersection `K ∩ A` is open in `K`,
then the space is a compactly coherent space. -/
lemma of_isOpen (h : ∀ (A : Set X), (∀ K, IsCompact K → IsOpen (K ↓∩ A)) → IsOpen A) :
    CompactlyCoherentSpace X where
  isCoherentWith := {isOpen_of_forall_induced := h}

/-- If every set `A` is closed if for every compact `K` the intersection `K ∩ A` is closed in `K`,
then the space is a compactly coherent space. -/
lemma of_isClosed (h : ∀ (A : Set X), (∀ K, IsCompact K → IsClosed (K ↓∩ A)) → IsClosed A) :
    CompactlyCoherentSpace X where
  isCoherentWith := IsCoherentWith.of_isClosed h

/-- Every weakly locally compact space is a compactly coherent space. -/
instance of_weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace X] : CompactlyCoherentSpace X where
  isCoherentWith := IsCoherentWith.of_nhds exists_compact_mem_nhds

@[deprecated (since := "2025-05-30")] alias
_root_.Topology.IsCoherentWith.isCompact_of_weaklyLocallyCompact := of_weaklyLocallyCompactSpace

/-- Every sequential space is a compactly coherent space. -/
instance of_sequentialSpace [SequentialSpace X] : CompactlyCoherentSpace X where
  isCoherentWith := IsCoherentWith.of_seq fun _u _x hux ↦ hux.isCompact_insert_range

@[deprecated (since := "2025-05-30")] alias
_root_.Topology.IsCoherentWith.isCompact_of_seq := of_sequentialSpace

/-- In a compactly coherent space `X`, a set `s` is open iff `f ⁻¹' s` is open for every continuous
map from a compact space. -/
lemma isOpen_iff_forall_compactSpace [CompactlyCoherentSpace X] (s : Set X) :
    IsOpen s ↔
      ∀ (K : Type u) [TopologicalSpace K] [CompactSpace K],
      ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s) := by
  refine ⟨fun hs _ _ _ _ hf ↦ hs.preimage hf, fun hs ↦ isOpen_iff |>.mpr ?_⟩
  intro K hK
  have : CompactSpace K := isCompact_iff_compactSpace.mp hK
  exact hs K Subtype.val continuous_subtype_val

/-- A topological space `X` is compactly coherent if a set `s` is open when `f ⁻¹' s?` is open for
every continuous map `f : K → X`, where `K` is compact. -/
lemma of_isOpen_forall_compactSpace (h : ∀ (s : Set X), (∀ (K : Type u) [TopologicalSpace K],
      [CompactSpace K] → ∀ (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) :
    CompactlyCoherentSpace X := by
  refine of_isOpen fun A hA ↦ h A fun K _ _ f hf ↦ ?_
  specialize hA (range f) (isCompact_range hf)
  have := hA.preimage (hf.codRestrict mem_range_self)
  rwa [← preimage_comp] at this

end CompactlyCoherentSpace
